Correctness by Construction(CxC)
構築からの正しさ(Correctness by Construction(CxC))
『ソフトウェア工学の道具としての形式手法 Formal Methods as Software Engineering Tools』
リファインメントは，段階的詳細化の方法を採用し， 宣言的に表現された正しい仕様から出発してプログラム として実現可能な記述に変換する。変換の各ステップで， 正しさが保存されることを形式検証する．正しい仕様か ら正しさが保証された変換を経て導出されたプログラム は正しさを保証されている。
ref: 形式手法の潮流 : アーキテクチャへの関心(<特集>システム設計のための形式手法の基礎と応用)P310
参考
『ソフトウェア工学の道具としての形式手法 Formal Methods as Software Engineering Tools』
中島 震. 形式手法の潮流 一アーキテクチャへの関心, 2008
形式手法の潮流 : アーキテクチャへの関心(<特集>システム設計のための形式手法の基礎と応用)
関連
詳細化(リファインメント)